""" This module contains all specifications of pi-graphs, used for testing.
"""

#========== BASIC PI-GRAPH SPECIFICATIONS ==========

Mono = """
[ 
    r[2] :! new(b) {
        a<b>.{}
    } 
]
"""

Spaw = """
[ 
    r[2] :! {a(x).{tau.{}}} 
]
"""

Term = """
[ 
    r[2] :! {a(x).{tau.{}}} 
]
"""

# Norm
Norm = '''
[
    r[2] :! {
        a(x).{tau.{tau.{}}} +
        tau.{}
    }

]
'''

Spaw_Norm_1 = '''
restricted a, c
[
    r[4] :! {
        a<b>.{ tau.{}  } +
        tau.{ c(x).{tau.{}} }
    }
]
'''

Spaw_Norm_2 = '''
[
    r1[2] :! {
        a<b>.{ tau.{}  }
    } ||

    r2[2] :! {
        [a=c]tau.{ c(x).{tau.{}} }
    }
]
'''

Norm_Spaw_1 = '''
[
    r[2] :! {
        c(x).{ tau.{}  } +
        [a=c][a=b]tau.{ a<b>.{tau.{}} }
    }
]
'''

Norm_Spaw_2 = '''
[
    r1[1] :! {
        c(x).{ tau.{}  }
    } ||

    r2[1] :! {
        [a=c][a=b]tau.{ a<b>.{tau.{}} }
    }
]
'''

Spaw_Spaw_1 = '''
restricted b
[
    r[2] :! {
        a(x).{tau.{}} +
        [a=c]c<b>.{tau.{}}
    }
]
'''

Spaw_Spaw_2 = '''
restricted b
[
    r1[2] :! {
        a(x).{tau.{}}
    }||

    r2[2] :! {
        [a=c]c<b>.{tau.{}}
    }
]
'''

# has no sync if a is a new name
Term_Norm_1 = '''
restricted b
[
    r[3] :! new(a){
        tau.{ a<b>.{} } +
        tau.{a(x).{tau.{}}}
    }
]
'''

Term_Norm_2 = '''
restricted a
[
    r1[2] :! new(b){
        tau.{ a<b>.{} }
    }||

    r2[1] :! {
        tau.{a(x).{tau.{}}}
    }
]
'''

Norm_Term_1 = '''
restricted a
[
    r[3] :! {
        tau.{ a(x).{} } +
        tau.{a<b>.{[a=b]tau.{}}}
    }
]
'''

Norm_Term_2 = '''
restricted a
[
    r1[2] :! {
        tau.{ a(x).{} }
    }||

    r2[3] :! {
        tau.{a<b>.{[a=b]tau.{}}}
    }
]
'''

Term_Term_1 = '''
restricted a
[
    r[3] :! {
        tau.{a(x).{}} +
        tau.{a<c>.{}}
    }
]
'''

Term_Term_2 = '''
restricted a
[
    r1[3] :! {
        tau.{a(x).{}}
    }||

    r2[2] :! new(c){
        tau.{a<c>.{}}
    }
]
'''

Term_Term_3 = '''
restricted a
[
    r[3] :! {
        tau.{ a(x).{} + a<c>.{}}
    }
]
'''

Spaw_Term_1 = '''
[
    r[2] :! {
        a<m>.{tau.{b(x).{}}}
    }
]
'''

Spaw_Term_2 = '''
[
    r1[2] :! {
        a<b>.{tau.{}}
    } ||

    r2[2] :! {
        tau.{b(x).{}}
    }
]
'''

Term_Spaw_1 = '''
restricted a
[
    r[1] :! {
        tau.{a<b>.{}} +
        a(x).{tau.{}}
    }
]
'''

Term_Spaw_2 = '''
restricted a
[
    r1[3] :! {
        tau.{a<b>.{}}
    }||

    r2[2] :! {
        a(x).{tau.{}}
    }
]
'''

Mono_Norm_1 = '''
restricted a
[
    r[3] :! {
        a<b>.{} +
        tau.{a(x).{tau.{}}}
    }
]
'''

Mono_Norm_2 = '''
restricted a
[
    r1[2] :! {
        a<b>.{}
    }||

    r2[2] :! {
        tau.{a(x).{tau.{}}}
    }
]
'''

Norm_Mono_1 = '''
restricted a
[
    r[3] :! {
        a(x).{} +
        tau.{a<b>.{tau.{}}}
    }
]
'''

Norm_Mono_2 = '''
restricted a
[
    r1[2] :! {
        a(x).{}
    }||

    r2[3] :! {
        tau.{a<b>.{tau.{}}}
    }
]
'''

Mono_Mono_1 = '''
[
    r[3] :! {
        a<b>.{} +
        a(x).{}
    }
]
'''


Mono_Mono_2 = '''
[
    r1[2] :! {
        a(x).{}
    }||
 
    r2[2] :! {
        a<b>.{}
    }
]
'''

Mono_Spaw_1 = '''
[
    r[3] :! {
        a<b>.{} +
        c(x).{tau.{}}
    }
]
'''

Mono_Spaw_2 = '''
[
    r1[2] :! {
        a<b>.{}
    } ||
    
    r2[2] :! {
        c(x).{tau.{}}
    }
]
'''

Spaw_Mono_1 = '''
[
    r[2] :! {
        a<b>.{tau.{}} +
        c(x).{}
    }
]
'''

Spaw_Mono_2 = '''
[
    r1[2] :! {
        a<b>.{tau.{}}
    } ||
    
    r2[3] :! {
        c(x).{}
    }
]
'''

Mono_Term_1 = '''
[
    r[3] :! {
        a<b>.{} +
        [a=c]tau.{c(x).{}}
    }
]
'''

Mono_Term_2 = '''
[
    r1[2] :! {
        a<b>.{}
    } ||
    
    r2[2] :! {
        [a=c]tau.{c(x).{}}
    }
]
'''

Term_Mono_1 = '''
restricted a
[
    r[3] :! {
        tau.{a<b>.{}} +
        a(x).{}
    }
]
'''

Term_Mono_2 = '''
restricted a
[
    r1[3] :! {
        tau.{a<b>.{}}
    }||
    
    r2[2] :! {
        a(x).{}
    }
]
'''

Norm_Norm_1 = '''
restricted a
[
    r[3] :! {
        tau.{a<b>.{tau.{}}} +
        tau.{a(x).{tau.{}}}
    }
]
'''

Norm_Norm_2 = '''
restricted a
[
    r1[2] :! {
        tau.{a<b>.{tau.{}}}
    }||
    
    r2[3] :! {
        tau.{a(x).{tau.{}}}
    }
]
'''

Norm_Norm_3 = '''
restricted a
[
    r[3] :! {
        tau.{ a<b>.{tau.{}} + a(x).{tau.{}}  }
    }
]
'''

Rec1 = '''
[
    r[2] :! new(k){
        a<b>.{b(x).{}}
    }
]
'''

Rec2 = '''
[
    r[1] :! {
        a(x).{tau.{a<b>.{}}}
    }
]
'''

PrivateSync = '''
restricted a, b
[
    r[2] :! {
        tau.{a(x).{}} +
        tau.{a<b>.{}}
    }    
]
'''

#========== OTHER PI-GRAPH SPECIFICATIONS ==========

# This specification contains all kinds of transitions
AllCases = """
[
    r1[2] :! {
        a<m>.{a<n>.{a(x).{}}} +
        a(y).{} +
        a<n>.{} +
        a(x).{a(y).{a<b>.{}}}
    } ||

    r2[2] :! {
        a(x).{a(y).{a<m>.{}}} +
        a<n>.{}+
        a(y).{a(m).{}}
    }
]
"""

# This is the example in the report
RptExample = '''
[
    r[2] :! {
        d(x).{
            [x=a]c<x>.{tau.{}} +
            [x <> a]c<a>.{}
        }
    }    
]
'''

# ERROR !!!!
Error_01 = '''
[
    r[2] :! {
        a<b>.{a(b).{b(x).{}}}
    }
]
'''

pingpong = '''
restricted a, b
[
    r0[1] :! {
        a<b>.{[a=b][a<>b]tau.{}}
    } ||
    
    r1[1] :! {
        a(x).{x<b>.{}}
    } ||
    
    r2[1] :! {
        b(y).{y<b>.{}}
    }
]
'''

fail01 = '''
[
    r1[1] :! new(b){
        tau.{a<b>.{}}
    } ||
    
    r2[1] :! {
        tau.{c(x).{tau.{}}}
    }
]
'''

s = '''
[
    r[2] :! {
        a(x).{b<y>.{}} +
        tau.{}
    }

]
'''

specialcase1 = """
[
    r[1] :! {
        c(x).{[a<>x]tau.{x<x>.{}}} +
        a(y).{d<y>.{}}
    }
]
"""

specialcase2 = """
[
    r[1] :! {
        c(x).{[a=x]tau.{x<x>.{}}} +
        a(y).{d<y>.{}}
    }
]
"""


s1 = """
restricted a
[
    r[2] :! {
        tau.{
            a(x).{tau.{}}
            +a<m>.{tau.{}}
        }
    }
]
"""

s2 = '''
[
    r[2]:! {
        tau.{a(x).{} + c<b>.{}}
    }
]
'''